\begin{tabbing}
es{-}only{-}sender(${\it es}$; $k$; $B$; $l$; ${\it tg}$; $T$; $s$,$v$.$f$($s$;$v$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:es{-}E(${\it es}$).\+\+
\\[0ex](es{-}loc(${\it es}$; $e$) = source($l$) $\in$ Id)
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd)
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd) c$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$)))))
\-\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex](es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ \=((es{-}kind(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) = $k$ $\in$ Knd)\+
\\[0ex]c$\wedge$ (es{-}valtype(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) $\subseteq$r $B$)
\\[0ex]c$\wedge$ (es{-}valtype(${\it es}$; ${\it e'}$) $\subseteq$r $T$)
\\[0ex]c$\wedge$ \=(\=es{-}val(${\it es}$; ${\it e'}$)\+\+
\\[0ex]=
\\[0ex]$f$(es{-}state{-}when(${\it es}$;es{-}sender(${\it es}$; ${\it e'}$));es{-}val(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)))
\\[0ex]$\in$ $T$
\-\\[0ex]\& (\=$\forall$${\it e''}$:es{-}E(${\it es}$).\+
\\[0ex](es{-}kind(${\it es}$; ${\it e''}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ (es{-}sender(${\it es}$; ${\it e''}$) = es{-}sender(${\it es}$; ${\it e'}$) $\in$ es{-}E(${\it es}$))
\\[0ex]$\Rightarrow$ (${\it e''}$ = ${\it e'}$ $\in$ es{-}E(${\it es}$))))))
\-\-\-\-\-
\end{tabbing}